Generalize integration_by_parts by IshiguroYoshihiro · Pull Request #1674 · math-comp/analysis

IshiguroYoshihiro · 2025-07-04T08:24:46Z

Motivation for this change

Add a part of generalized version of integration by parts for unbound intervals `[a, +oo[.
This PR is over #1656 and #1662.
I don't sure that I should add 4 more lemmas and complete all variation of integration by parts for unbound intervals.
I think that 8 similar lemmas would be a mess. So, I'd like to somehow make them up into one or two lemmas, but I don't have an idea.

Checklist

added corresponding entries in CHANGELOG_UNRELEASED.md

added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

PRs with several commits that make sense individually and that
all compile are preferentially merged into master.
PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

Read this Checklist
Put a milestone if possible
Check labels

Tragicus · 2025-07-15T07:51:01Z

Are not all 4 versions the same, the only difference being whether the minus is inside or outside the integral?

IshiguroYoshihiro · 2025-07-28T07:15:45Z

Are not all 4 versions the same, the only difference being whether the minus is inside or outside the integral?

If you said that these lemmas can be proved with one of them, I think it is no.
As you can see, the version of le0_ge0 and le0_le0 can be proved with ge0_ge0 or ge0_le0, but ge0_le0 can not proved from ge0_ge0.
Because that integration by substitusion using a transformation F -> F \o -%R change the unbounded side of the interval from `[a, +oo[ to `[-oo, - a[, I may have to set 4 more variations of this lemma for `[-oo, -a[.
It will makes messy for the use to set 8 variation of the lemma. So I will consider some good way.

affeldt-aist · 2025-10-30T09:35:48Z

Are not all 4 versions the same, the only difference being whether the minus is inside or outside the integral?

Indeed le0_le0 is the same as ge0_ge0 (and it is proved as such).
Similarly, for ge0_le0 vs. le0_ge0.
I don't think we can have more sharing.
Do you think that we should work towards a general version? A single lemma encompassing them all?

affeldt-aist · 2025-10-30T09:37:11Z

Are not all 4 versions the same, the only difference being whether the minus is inside or outside the integral?

Indeed le0_le0 is the same as ge0_ge0 (and it is proved as such). Similarly, for ge0_le0 vs. le0_ge0. I don't think we can have more sharing. Do you think that we should work towards a general version? A single lemma encompassing them all?

To give a bit of context, these lemmas have been written this way after having been tested to formalize the Gamma function. Maybe their apparent specialization is the result of practical considerations? @IshiguroYoshihiro can you confirm? (Or am I remembering wrong?)

Tragicus

Sorry, I am back.
One way to factorize would be to ask for the relevant functions to have constant sign. I was also wondering whether we want to generalize over the interval, instead of [a, +oo[. We would require that the relevant functions are derivable on the interior of the interval and have limits at the boundaries.
@affeldt-aist Some of the following suggestions are quite ugly but save a lot of time, what do you think?

theories/ftc.v

Tragicus · 2025-11-03T13:53:25Z

theories/ftc.v

+rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//.
+- rewrite oppeD; last exact: fin_num_adde_defr.
+  rewrite -EFinN opprD 2!opprK mulNr.
+  by under eq_integral do rewrite mulNr EFinN oppeK.
+- by move=> ?; apply: cvgN; exact: cf.
+- exact: derivable_oy_continuous_bndN.
+- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.


Suggested change

rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//.

- rewrite oppeD; last exact: fin_num_adde_defr.

rewrite -EFinN opprD 2!opprK mulNr.

by under eq_integral do rewrite mulNr EFinN oppeK.

- by move=> ?; apply: cvgN; exact: cf.

- exact: derivable_oy_continuous_bndN.

- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.

rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//.

- rewrite oppeD; last exact: fin_num_adde_defr.

rewrite -EFinN opprD 2!opprK mulNr.

by under eq_integral do rewrite mulNr EFinN oppeK.

- by move=> ?; apply: cvgN; exact: cf.

- exact: derivable_oy_continuous_bndN.

- by move=> ? ?; rewrite fctE derive1N ?Ff => [//|//|]; apply: Foy.1.

.6s faster

theories/realfun.v

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

affeldt-aist · 2025-11-21T16:01:18Z

To give a bit of context, these lemmas have been written this way after having been tested to formalize the Gamma function.

FYI, here is the PR that formalizes the Gamma function:
#1762

One way to factorize would be to ask for the relevant functions to have constant sign. I was also wondering whether we want to generalize over the interval, instead of [a, +oo[. We would require that the relevant functions are derivable on the interior of the interval and have limits at the boundaries.

This has not been tested yet (by lack of time). :-(

Some of the following suggestions are quite ugly but save a lot of time, what do you think?

We have merged all of them. Thanks for identifying the performance issues, that helps.

theories/ftc.v

t6s · 2025-12-11T07:52:49Z

I suggest keeping 4 lemmas as is, and additionally, provide a unified interface lemma that use the constant_sign predicate

theories/ftc.v

t6s · 2026-01-13T07:40:00Z

looking at the code for a while, I noticed there can be some helper lemmas added:

Lemma seqDU0 : forall {T : Type} (F : (set T)^nat), seqDU F 0%N = F 0%N.
Proof. by move=> ? ?; rewrite /seqDU/= big_ord0 setD0. Qed.

Lemma seqDU1_itv : forall {R : realDomainType} (r : R) b1 b2,
  seqDU (fun n => [set` Interval (BSide b1 r) (BSide b2 (r + n%:R))]) 1 =
  [set` Interval (BSide (b1 && b2) r) (BSide b2 (r + 1%:R))].
Proof.
move=> ? r b1 b2.
rewrite /seqDU big_ord1/= addr0 setDE.
case: b1; case: b2; rewrite (set_itvco0,set_itv1,set_itvoo0,set_itvoc0) ?setC0 ?setIT//.
by rewrite -setDE setDitv1l.
Qed.

Lemma seqDUSn_itv_notoo : forall {R : realDomainType} n (r : R) b1 b2,
  (b1 == true) || (b2 == false) -> (* not a seqDU of open intervals *)
  seqDU (fun n => [set` Interval (BSide b1 r) (BSide b2 (r + n%:R))]) n.+1 =
  [set` Interval (BSide b2 (r + n%:R)) (BSide b2 (r + n.+1%:R))].
Proof.
move=> ? n r b1 b2 b12.
rewrite seqDU_seqD; last first.
  apply/nondecreasing_seqP => k; apply/subsetPset/subset_itvl.
  by rewrite bnd_simp lerD2l ler_nat.
rewrite eqEsubset; split => x /= /[!in_itv] /=.
  move=> [] /andP[-> ->] /[!andbT] /= /negP.
  clear b12.
  by case: b1; case: b2; rewrite /= -?ltNge -?leNgt.
move=> /andP[rnx ->]; rewrite andbT; split.
  move: b12.
  case: b1 => /=.
    by move=> _; have/lteifW/(le_trans _) := rnx; apply; rewrite lerDl.
  by move: rnx; case: b2 => //= + _  => /(le_lt_trans _); apply; rewrite lerDl.
by apply/negP; rewrite negb_and [X in _ || X]lteifN ?negbK// orbT.
Qed.

Lemma seqDUSSn_itv : forall {R : realDomainType} n (r : R) b1 b2,
  seqDU (fun n => [set` Interval (BSide b1 r) (BSide b2 (r + n%:R))]) n.+2 =
  [set` Interval (BSide b2 (r + n.+1%:R)) (BSide b2 (r + n.+2%:R))].
Proof.
move=> ? n r b1 b2.
case/boolP: ((b1 == true) || (b2 == false)); first by move/seqDUSn_itv_notoo.
case: b1; case: b2 => // _.
rewrite seqDU_seqD; last first.
  apply/nondecreasing_seqP => k; apply/subsetPset/subset_itvl.
  by rewrite bnd_simp lerD2l ler_nat.
rewrite eqEsubset; split => x /= /[!in_itv] /=.
  by move=> [] /andP[-> ->] /[!andbT] /= /negP; rewrite -leNgt.
move=> /andP[rnx ->].
rewrite andbT; split; first by rewrite (lt_le_trans _ rnx)// ltrDl.
by apply/negP; rewrite negb_and -!leNgt rnx orbT.
Qed.

Lemma set_itv_Sset1 :
  forall [disp : Order.disp_t] [T : porderType disp] (x : T) b1 b2 ,
    [set` Interval (BSide b1 x) (BSide b2 x)] `<=` [set x].
Proof.
move=> ? ? ? b1 b2.
by case: b1; case: b2; rewrite (set_itv1,set_itvoo0,set_itvxx).
Qed.

Lemma seqDUn_sSet_itvcc : forall {R : realDomainType} n (r : R) b1 b2,
  seqDU (fun n => [set` Interval (BSide b1 r) (BSide b2 (r + n%:R))]) n `<=`
    `[r + n.-1%:R, r + n%:R].
Proof.
move=> ? n r b1 b2.
case: n => [|n /=].
  by rewrite seqDU0 addr0; apply: subset_itvScc; rewrite bnd_simp.
case: n => [|n /=].
  by rewrite seqDU1_itv addr0; apply: subset_itvScc; rewrite bnd_simp.
by rewrite seqDUSSn_itv; apply: subset_itvScc; rewrite bnd_simp.
Qed.

(* generalizations of lemmas of the same names *)
Lemma integral_itv_obnd_cbnd :
  forall {R : realType} [r : R] [b : itv_bound R] [f : R -> R] lr,
    measurable_fun [set` Interval (BRight r) b] f ->
    \int[mu]_(x in [set` Interval (BSide lr r) b]) (f x)%:E =
    \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E.
Proof. by move=> ? ? ? ?; case; [by []|exact: integral_itv_obnd_cbnd]. Qed.

Lemma integral_itv_bndo_bndc :
  forall {R : realType} [a : itv_bound R] [r : R] [f : R -> R] lr,
    measurable_fun [set` Interval a (BLeft r)] f ->
    \int[mu]_(x in [set` Interval a (BSide lr r)]) (f x)%:E =
    \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E.
Proof. by move=> ? ? ? ?; case; [exact: integral_itv_bndo_bndc|by []]. Qed.

Lemma measurable_fun_itv_bnd :
  forall [R : realType] [x y : R] [b1 b2 b3 b4 : bool] [f : R -> R],
  measurable_fun [set` Interval (BSide b1 x) (BSide b2 y)] f ->
  measurable_fun [set` Interval (BSide b3 x) (BSide b4 y)] f.
Proof.
move=> ? x y ? ? ? ? ? f_measurable.
apply: (measurable_funS `[x, y]) => //.
  by apply: subset_itvScc; rewrite bnd_simp.
exact: (measurable_fun_itv_cc f_measurable).
Qed.

Lemma integral_itv_bnd :
  forall {R : realType} [x y : R] [f : R -> R] (b1 b2 b3 b4 : bool),
  measurable_fun `]x, y[ f ->
  \int[mu]_(z in [set` Interval (BSide b1 x) (BSide b2 y)]) (f z)%:E =
  \int[mu]_(z in [set` Interval (BSide b3 x) (BSide b4 y)]) (f z)%:E.
Proof.
move=> ? x y ? ? ? ? ? f_measurable.
do 2 (rewrite integral_itv_bndo_bndc; last exact: (measurable_fun_itv_bnd f_measurable)).
do 2 (rewrite integral_itv_obnd_cbnd; last exact: (measurable_fun_itv_bnd f_measurable)).
by [].
Qed.

Lemma integral_itv_bndcc :
  forall {R : realType} [x y : R] [f : R -> R] (b1 b2: bool),
  measurable_fun `]x, y[ f ->
  \int[mu]_(z in [set` Interval (BSide b1 x) (BSide b2 y)]) (f z)%:E =
  \int[mu]_(z in `[x, y]) (f z)%:E.
Proof. move=> *; exact: integral_itv_bnd. Qed.

t6s · 2026-01-13T07:40:48Z

Section integralN.
Local Open Scope order_scope.

Lemma lef0_integralN
  {d : measure_display} {T : measurableType d} {R : realType} {mu : measure T R}
  (D : set T) (f : T -> \bar R) :
  d.-measurable D ->
  {in D, forall x, f x <= 0} ->
  (\int[mu]_(x in D) - f x)%E = (- (\int[mu]_(x in D) f x))%E.
Proof.
move=> mD lef0; rewrite integralN// fin_num_adde_defr//.
under eq_integral => ? ?.
  by rewrite (le0_funeposE lef0); first over; rewrite inE.
by rewrite integral_cst// mul0e.
Qed.

Lemma le0f_integralN
  {d : measure_display} {T : measurableType d} {R : realType} {mu : measure T R}
  (D : set T) (f : T -> \bar R) :
  d.-measurable D ->
  {in D, forall x, 0%E <= f x} ->
  (\int[mu]_(x in D) - f x)%E = (- (\int[mu]_(x in D) f x))%E.
Proof.
move=> mD le0f; rewrite integralN// fin_num_adde_defl//.
under eq_integral => ? ?.
  by rewrite (ge0_funenegE le0f); first over; rewrite inE.
by rewrite integral_cst// mul0e.
Qed.

End integralN.

t6s · 2026-01-13T07:42:52Z

leading to generalization of sum_integral_limn:

Let sumN_Nsum_fG n b1 b2 :
  (b1 == true) || (b2 == false) ->
  \sum_(0 <= i < n)
    (- (\int[mu]_(x in seqDU (fun k => [set` Interval (BSide b1 a) (BSide b2 (a + k%:R))]) i)
         (f x * G x)%:E))%E =
  - (\sum_(0 <= i < n)
      (\int[mu]_(x in seqDU (fun k => [set` Interval (BSide b1 a) (BSide b2 (a + k%:R))]) i)
        (f x * G x)%:E)%E).
Proof.
move=> b12.
rewrite big_nat_cond fin_num_sumeN -?big_nat_cond// => m _.
case: m => [|m].
  by rewrite seqDU0 addr0 (integral_Sset1 a)//; exact: set_itv_Sset1.
rewrite seqDUSn_itv_notoo//.
rewrite integral_itv_bndcc; last first.
  apply: (measurable_funS `[a, +oo[) => //.
  by apply/subset_itv => //; rewrite bnd_simp// lerDl.
apply: integrable_fin_num => //=.
apply: continuous_compact_integrable; first exact: segment_compact.
apply: continuous_subspaceW cfG.
by apply: subset_itv; rewrite // bnd_simp// lerDl.
Qed.

Let sum_integral_limn b1 b2 :
  (b1 == true) || (b2 == false) ->
  \sum_(0 <= i <oo)
    \int[mu]_(x in seqDU (fun k => [set` Interval (BSide b1 a) (BSide b2 (a + k%:R))]) i) (F x * g x)%:E
  = limn (fun n => (F (a + n.-1%:R) * G (a + n.-1%:R) - F a * G a)%:E
                    + \sum_(0 <= i < n)
                    - \int[mu]_(x in seqDU (fun k => [set` Interval (BSide b1 a) (BSide b2 (a + k%:R))]) i)
                        (f x * G x)%:E).
Proof.
move=> b12.
apply/congr_lim/funext; case.
  by rewrite big_nat_cond [in RHS]big_nat_cond 2?big_pred0//= 2!addr0 subrr.
case=> [|n].
  rewrite 2!big_nat1 seqDU0 -pred_Sn addr0 subrr add0r.
  rewrite !(integral_Sset1 a) ?oppe0//; exact: set_itv_Sset1.
rewrite big_nat_recl// [in RHS]big_nat_recl//=.
rewrite seqDU0 addr0 !(integral_Sset1 a); [|exact: set_itv_Sset1|exact: set_itv_Sset1].
rewrite oppe0 2!add0r.
under eq_bigr => i _.
  rewrite seqDUSn_itv_notoo//= (integral_itv_bndcc b2 b2); last first.
    apply: (measurable_funS `[a, +oo[) => //.
    by apply/subset_itv => //; rewrite bnd_simp lerDl.
  rewrite (integration_by_parts _ _ _ (@Ffai i) _ _ (@Ggai i)); last 5 first.
  - by rewrite ltrD2l ltr_nat.
  - apply: continuous_subspaceW cf.
    by apply/subset_itv => //; rewrite bnd_simp lerDl.
  - apply: derivable_oy_continuousWoo Foy.
    + by rewrite ltrD2l ltr_nat.
    + by rewrite lerDl.
  - apply: continuous_subspaceW cg.
    by apply/subset_itv => //; rewrite bnd_simp lerDl.
  - apply: derivable_oy_continuousWoo Goy.
    + by rewrite ltrD2l ltr_nat.
    + by rewrite lerDl.
  over.
rewrite big_split/=.
under eq_bigr do rewrite EFinB.
rewrite telescope_sume => [|//|//]; rewrite addr0; congr +%E.
apply: eq_bigr => k _; rewrite seqDUSn_itv_notoo; last by [].
rewrite [in RHS]integral_itv_bndcc; first by [].
apply: measurable_funS mfG => //.
by apply/subset_itv => //; rewrite bnd_simp lerDl.
Qed.

affeldt-aist · 2026-01-13T07:44:03Z

looking at the code for a while, I noticed there can be some helper lemmas added:
...

on our side, we were trying to get rid of seqDU that does not seem to be here for good reasons :-/

t6s · 2026-01-13T07:47:43Z

looking at the code for a while, I noticed there can be some helper lemmas added:
...

on our side, we were trying to get rid of seqDU that does not seem to be here for good reasons :-/

that sounds better

t6s · 2026-01-13T08:34:41Z

I suggest keeping 4 lemmas as is, and additionally, provide a unified interface lemma that use the constant_sign predicate

I have changed my mind to endorse constant_sign, as this notion can be handily expressed
by (f <= 0) || (0 <= f) using FunOrder.lef, and moreover, it contradicts Num.sgr.

t6s

The main lemmas look good.
After trying to remove subset_itvoSo_cSc, this PR will be ready for merging.

t6s · 2026-01-13T08:46:24Z

reals/real_interval.v


 End itv_realDomainType.

+(* generalization of


This lemma can be an instance of the monotonicity of the closure operator.

t6s · 2026-01-13T08:47:07Z

theories/ftc.v

+
+End integration_by_partsy_ge0.
+
+Section integration_by_partsy_le0.


This section appears to be sharing many things with the previous one.
Maybe merge the two?

affeldt-aist · 2026-01-15T01:50:49Z

Even though we are making progress, in the interest of the release, I would like to postpone to the next release (that will happen anyway faster than this one). Thank for your understanding.

t6s · 2026-01-17T16:56:40Z

IshiguroYoshihiro#69 rebased onto master

IshiguroYoshihiro and others added 2 commits October 30, 2025 15:46

integration_by_party

cdc9e90

upd and rebase

0802b9c

affeldt-aist force-pushed the integration_by_partsy_20250704 branch from 949b179 to 0802b9c Compare October 30, 2025 07:07

lint

675d017

affeldt-aist marked this pull request as ready for review October 30, 2025 09:32

Tragicus reviewed Nov 3, 2025

View reviewed changes

affeldt-aist added this to the 1.15.0 milestone Nov 4, 2025

affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Nov 4, 2025

affeldt-aist and others added 18 commits November 18, 2025 11:01

Update theories/ftc.v

51221f8

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

416f04e

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

ee10e62

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

1d4fad1

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

e1f402d

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

56962a5

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

29e41af

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

bbfb611

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

1c8a7bd

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

6d64684

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

13d160a

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

d3ae241

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

2cc1eaf

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

8132f6b

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

2b869ba

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

42b28b4

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

2f5767f

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/ftc.v

7facd27

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

Update theories/realfun.v

66bb713

Co-authored-by: Quentin VERMANDE <quentin.vermande@orange.fr>

IshiguroYoshihiro mentioned this pull request Nov 18, 2025

the Gamma function #1762

Open

2 tasks

t6s reviewed Dec 11, 2025

View reviewed changes

theories/ftc.v Show resolved Hide resolved

t6s reviewed Dec 14, 2025

View reviewed changes

theories/ftc.v Outdated Show resolved Hide resolved

affeldt-aist reviewed Dec 24, 2025

View reviewed changes

theories/ftc.v Outdated Show resolved Hide resolved

affeldt-aist reviewed Dec 24, 2025

View reviewed changes

theories/ftc.v Outdated Show resolved Hide resolved

IshiguroYoshihiro and others added 4 commits January 9, 2026 12:12

fix

c4b4caf

minor fix

04e62f3

wip cleaning Let

a6c88a7

prove admit

34697b2

affeldt-aist force-pushed the integration_by_partsy_20250704 branch from 5036126 to 34697b2 Compare January 13, 2026 07:34

t6s reviewed Jan 13, 2026

View reviewed changes

affeldt-aist modified the milestones: 1.15.0, 1.16.0 Jan 15, 2026


		End integration_by_partsy_ge0.

		Section integration_by_partsy_le0.

Conversation

IshiguroYoshihiro commented Jul 4, 2025

Motivation for this change

Checklist

Merge policy

Reminder to reviewers

Uh oh!

Tragicus commented Jul 15, 2025

Uh oh!

IshiguroYoshihiro commented Jul 28, 2025

Uh oh!

affeldt-aist commented Oct 30, 2025

Uh oh!

affeldt-aist commented Oct 30, 2025

Uh oh!

Tragicus left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Tragicus Nov 3, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

affeldt-aist commented Nov 21, 2025

Uh oh!

Uh oh!

t6s commented Dec 11, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

t6s commented Jan 13, 2026

Uh oh!

t6s commented Jan 13, 2026

Uh oh!

t6s commented Jan 13, 2026

Uh oh!

affeldt-aist commented Jan 13, 2026

Uh oh!

t6s commented Jan 13, 2026

Uh oh!

t6s commented Jan 13, 2026

Uh oh!

t6s left a comment

Choose a reason for hiding this comment

Uh oh!

t6s Jan 13, 2026

Choose a reason for hiding this comment

Uh oh!

t6s Jan 13, 2026

Choose a reason for hiding this comment

Uh oh!

affeldt-aist commented Jan 15, 2026

Uh oh!

t6s commented Jan 17, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants